weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== ((x:Id. vartype(source(l);x) r ds(x)?Top)
== & e@source(l). (kind(e) = locl(a))  (valtype(e) r A)
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r T)))
== c ((e':E.
== c (((kind(e') = rcv(l,tg))
== c (( ((kind(sender(e')) = locl(a))
== c (( c (((P((state when sender(e')))))
== c (( c & val(e') = f((state when sender(e')),val(sender(e'))))))
== c & e@source(l).
== c & e':E
== c & (e c e'
== c & & (((kind(e') = rcv(l,tg)) c e loc sender(e') )
== c & & ( ((loc(e') = source(l)) c ((t:. (P((state after e')+t)))))))) 

latex

---

clarification:

weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)
== ((x:Id. es-vartype(es; source(l); x) r fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;source(l);e.(es-kind(es; e) = locl(a)  Knd)  (es-valtype(es; e) r A))
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r T)))
== c ((e':es-E(es).
== c (((es-kind(es; e') = rcv(l,tg)  Knd)
== c (( ((es-kind(es; es-sender(es; e')) = locl(a)  Knd)
== c (( c (((P(es-state-when(es;es-sender(es; e')))))
== c (( c & es-val(es; e')
== c (( c & =
== c (( c & f(es-state-when(es;es-sender(es; e')),es-val(es; es-sender(es; e')))
== c (( c &  T)))
== c & alle-at(es;source(l);e.e':es-E(es)
== c & alle-at(es;source(l);e.(es-causle(es;e;e')
== c & alle-at(es;source(l);e.& (((es-kind(es; e') = rcv(l,tg)  Knd)
== c & alle-at(es;source(l);e.& (c es-le(es;e;es-sender(es; e')))
== c & alle-at(es;source(l);e.& ( ((es-loc(es; e') = source(l)  Id)
== c & alle-at(es;source(l);e.& ( c ((t:. (P(es-state-after-elapsed(es;e';t)))))))))) 

latex

Definitions	vartype(i;x), f(x)?z, IdDeq, Top, valtype(e), P  Q, locl(a), (state when e), val(e), e@i. P(e), x:A. B(x), E, P & Q, e c e', P  Q, Knd, kind(e), rcv(l,tg), e loc e' , sender(e), A c B, s = t, Id, loc(e), source(l), A, x:A. B(x), , b, f(a), (state after e)+t
FDL editor aliases	weak-precond-send-p